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