Bob is cold. Bob is green. Bob is nice. Bob is rough. Bob is smart. Charlie is nice. Fiona is furry. Fiona is green. Fiona is nice. Fiona is white. If something is smart then it is furry. Furry, cold things are smart. Green, smart things are white. If something is cold then it is white. If something is nice and white then it is smart. Smart, green things are white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Furry, cold things are smart.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Green, smart things are white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is nice and white then it is smart.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Smart, green things are white.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Fiona is furry.
True
1
proof
[(triple7 OR ((((triple9 triple10) -> rule5)) -> rule1))]
("Fiona" "is" "furry" "+")
triple7
((((triple9 triple10) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not white.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "white" "-")
triple10
Bob is white.
True
2
proof
[(((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((triple5 triple2) -> rule6))]
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((triple5 triple2) -> rule6))]
("Bob" "is" "white" "-")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is furry.
Unknown
rconc
[@3: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is rough.[(triple4)] Bob is smart.[(triple5 OR ((triple3 ((triple1) -> rule4)) -> rule5))] Charlie is nice.[(triple6)] Fiona is furry.[(triple7 OR ((((triple9 triple10) -> rule5)) -> rule1))] Fiona is green.[(triple8)] Fiona is nice.[(triple9)] Fiona is white.[(triple10)] @1: Bob is furry.[(((triple5) -> rule1) OR ((((triple3 ((triple1) -> rule4)) -> rule5)) -> rule1))] Bob is white.[(((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((triple5 triple2) -> rule6))] Fiona is smart.[(((triple9 triple10) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple3 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
((((triple9 triple10) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 triple5) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple5 triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9 triple10) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1