Bob is round. Fiona is big. Harry is rough. If Fiona is nice and Fiona is round then Fiona is young. If someone is young then they are rough. If Harry is round then Harry is nice. If someone is round then they are big. If someone is big then they are nice. If someone is big and round then they are blue.
Bob is round.
("Bob" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Fiona is nice and Fiona is round then Fiona is young.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "round" "+")) -> ("Fiona" "is" "young" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Harry is round then Harry is nice.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "nice" "+"))
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and round then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Fiona is nice.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is round.[(triple1)] Fiona is big.[(triple2)] Harry is rough.[(triple3)] @1: Bob is big.[(((triple1) -> rule4))] Fiona is nice.[(((triple2) -> rule5))] @2: Bob is blue.[(((((triple1) -> rule4) triple1) -> rule6))] Bob is nice.[(((((triple1) -> rule4)) -> rule5))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2