Bob is round. Dave is big. Dave is white. Fiona is rough. Fiona is white. Gary is big. Gary is white. Smart people are big. If someone is white then they are smart. If someone is big then they are blue. If Bob is rough then Bob is smart. If someone is blue and not white then they are not kind. Round, blue people are kind. If someone is blue and not rough then they are kind. If someone is rough and not smart then they are round.
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is white.
("Gary" "is" "white" "+")
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Bob is rough then Bob is smart.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "smart" "+"))
If someone is blue and not white then they are not kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "-"))
Round, blue people are kind.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and not rough then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "kind" "+"))
If someone is rough and not smart then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "round" "+"))
Fiona is rough.
True
1
proof
[(triple4)]
("Fiona" "is" "rough" "+")
triple4
Fiona is not white.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "white" "-")
triple5
Dave is smart.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "smart" "-")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is big.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Fiona" "is" "big" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("Fiona" "is" "big" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
True
4
proof
[(((((((triple5) -> rule2)) -> rule1)) -> rule3))]
("Fiona" "is" "blue" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not blue.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule1)) -> rule3))]
("Fiona" "is" "blue" "-")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "round" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "big" "+")
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is round.[(triple1)] Dave is big.[(triple2 OR ((((triple3) -> rule2)) -> rule1))] Dave is white.[(triple3)] Fiona is rough.[(triple4)] Fiona is white.[(triple5)] Gary is big.[(triple6 OR ((((triple7) -> rule2)) -> rule1))] Gary is white.[(triple7)] @1: Dave is blue.[(((triple2) -> rule3) OR ((((((triple3) -> rule2)) -> rule1)) -> rule3))] Dave is smart.[(((triple3) -> rule2))] Fiona is smart.[(((triple5) -> rule2))] Gary is blue.[(((triple6) -> rule3) OR ((((((triple7) -> rule2)) -> rule1)) -> rule3))] Gary is smart.[(((triple7) -> rule2))] @2: Fiona is big.[(((((triple5) -> rule2)) -> rule1))] @3: Fiona is blue.[(((((((triple5) -> rule2)) -> rule1)) -> rule3))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Fiona is white.
("Fiona" "is" "white" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3