Anne is cold. Anne is green. Anne is nice. Bob is young. Dave is green. Dave is nice. Dave is smart. Harry is big. Harry is blue. Harry is cold. If Anne is young and Anne is cold then Anne is green. All big, young things are smart. Young things are green. All green things are cold. If Anne is young and Anne is green then Anne is blue. If something is young then it is nice. All young, smart things are nice. If something is nice then it is young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Anne is young and Anne is cold then Anne is green.
((("Anne" "is" "young" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "green" "+"))
All big, young things are smart.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Anne is young and Anne is green then Anne is blue.
((("Anne" "is" "young" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "blue" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All young, smart things are nice.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Dave is not nice.
False
1
inv-proof
[(triple6)]
("Dave" "is" "nice" "-")
triple6
Bob is green.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "green" "+")
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple6) -> rule8))]
("Dave" "is" "young" "-")
((triple6) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Harry" "is" "young" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is cold.[(triple1 OR ((triple2) -> rule4) OR ((((((triple3) -> rule8)) -> rule3)) -> rule4))] Anne is green.[(triple2 OR ((((triple3) -> rule8)) -> rule3) OR ((((triple3) -> rule8) triple1) -> rule1))] Anne is nice.[(triple3)] Bob is young.[(triple4)] Dave is green.[(triple5 OR ((((triple6) -> rule8)) -> rule3))] Dave is nice.[(triple6)] Dave is smart.[(triple7)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10)] @1: Anne is young.[(((triple3) -> rule8))] Bob is green.[(((triple4) -> rule3))] Bob is nice.[(((triple4) -> rule6))] Dave is cold.[(((triple5) -> rule4) OR ((((((triple6) -> rule8)) -> rule3)) -> rule4))] Dave is young.[(((triple6) -> rule8))] @2: Anne is blue.[(((((triple3) -> rule8) triple2) -> rule5) OR ((((triple3) -> rule8) ((((triple3) -> rule8)) -> rule3)) -> rule5) OR ((((triple3) -> rule8) ((((triple3) -> rule8) triple1) -> rule1)) -> rule5))] Bob is cold.[(((((triple4) -> rule3)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple2
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple3) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple5) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple3) -> (rule8 % int2)) triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple3) -> (rule8 % int3)) ((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple3) -> (rule8 % int3)) ((((triple3) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2