Bob is blue. Bob is white. Fiona is red. Fiona is round. Fiona is white. Harry is round. Harry is white. If Harry is nice and Harry is round then Harry is white. If Harry is big and Harry is blue then Harry is round. If something is white then it is blue. Red, round things are not big. If Harry is young then Harry is not big. All blue things are not nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is nice and Harry is round then Harry is white.
((("Harry" "is" "nice" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
If Harry is big and Harry is blue then Harry is round.
((("Harry" "is" "big" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "round" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Red, round things are not big.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
If Harry is young then Harry is not big.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "big" "-"))
All blue things are not nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "-"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Fiona is not white.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "white" "-")
triple5
Fiona is not big.
True
3
proof
[(((triple3 triple4) -> rule4))]
("Fiona" "is" "big" "-")
((triple3 triple4) -> (rule4 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Harry is not blue.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "blue" "-")
((triple7) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule3))] Bob is white.[(triple2)] Fiona is red.[(triple3)] Fiona is round.[(triple4)] Fiona is white.[(triple5)] Harry is round.[(triple6)] Harry is white.[(triple7)] @1: Bob is not nice.[(((triple1) -> rule6) OR ((((triple2) -> rule3)) -> rule6))] Fiona is blue.[(((triple5) -> rule3))] Fiona is not big.[(((triple3 triple4) -> rule4))] Harry is blue.[(((triple7) -> rule3))] @2: Fiona is not nice.[(((((triple5) -> rule3)) -> rule6))] Harry is not nice.[(((((triple7) -> rule3)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Fiona is white.
("Fiona" "is" "white" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is not nice.
("Bob" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not big.
("Fiona" "is" "big" "-")
((triple3 triple4) -> (rule4 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2