Bob is smart. Charlie is blue. Dave is round. Harry is smart. If Harry is round then Harry is blue. Round, blue people are young. If someone is big then they are cold. All young, big people are blue. Smart people are blue. If someone is smart then they are round. If someone is round and rough then they are cold. All blue, smart people are big.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is round then Harry is blue.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "blue" "+"))
Round, blue people are young.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All young, big people are blue.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is round and rough then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
All blue, smart people are big.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple4)]
("Harry" "is" "smart" "-")
triple4
Bob is blue.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "blue" "-")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is big.
True
4
proof
[(((((triple4) -> rule5) triple4) -> rule8) OR ((((((triple4) -> rule6)) -> rule1) triple4) -> rule8))]
("Harry" "is" "big" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule8))]
("Bob" "is" "big" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
True
5
proof
[(((((((triple1) -> rule5) triple1) -> rule8)) -> rule3))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((((triple1) -> rule5) triple1) -> rule8)) -> rule3))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Dave" "is" "blue" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "young" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Charlie is blue.[(triple2)] Dave is round.[(triple3)] Harry is smart.[(triple4)] @1: Bob is blue.[(((triple1) -> rule5))] Bob is round.[(((triple1) -> rule6))] Harry is blue.[(((triple4) -> rule5) OR ((((triple4) -> rule6)) -> rule1))] Harry is round.[(((triple4) -> rule6))] @2: Bob is big.[(((((triple1) -> rule5) triple1) -> rule8))] Bob is young.[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule2))] Harry is big.[(((((triple4) -> rule5) triple4) -> rule8) OR ((((((triple4) -> rule6)) -> rule1) triple4) -> rule8))] Harry is young.[(((((triple4) -> rule6) ((triple4) -> rule5)) -> rule2) OR ((((triple4) -> rule6) ((((triple4) -> rule6)) -> rule1)) -> rule2))] @3: Bob is cold.[(((((((triple1) -> rule5) triple1) -> rule8)) -> rule3))] Harry is cold.[(((((((triple4) -> rule5) triple4) -> rule8)) -> rule3) OR ((((((((triple4) -> rule6)) -> rule1) triple4) -> rule8)) -> rule3))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule6 % int3)) ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple4) -> (rule6 % int3)) ((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule5 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple4) -> (rule6 % int4))) -> (rule1 % int3)) triple4) -> (rule8 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4