Bob is green. Bob is quiet. Bob is red. Bob is white. Fiona is blue. Fiona is quiet. Harry is red. If Fiona is blue then Fiona is green. Green, quiet things are big.
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If Fiona is blue then Fiona is green.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "green" "+"))
Green, quiet things are big.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Bob is big.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "big" "-")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is big.
True
4
proof
[(((((triple5) -> rule1) triple6) -> rule2))]
("Fiona" "is" "big" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((((triple5) -> rule1) triple6) -> rule2))]
("Fiona" "is" "big" "-")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is green.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Bob is white.[(triple4)] Fiona is blue.[(triple5)] Fiona is quiet.[(triple6)] Harry is red.[(triple7)] @1: Bob is big.[(((triple1 triple2) -> rule2))] Fiona is green.[(((triple5) -> rule1))] @2: Fiona is big.[(((((triple5) -> rule1) triple6) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2