Anne is big. Anne is not smart. Charlie is big. Charlie is red. Charlie is smart. Fiona is green. Fiona is red. Harry is not cold. Harry is smart. Harry is young. If something is red and white then it is big. If something is red then it is cold. All big things are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red and white then it is big.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Charlie is smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "+")
triple5
Harry is not young.
False
1
inv-proof
[(triple10)]
("Harry" "is" "young" "-")
triple10
Fiona is cold.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple4) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Anne is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is not smart.[(triple2)] Charlie is big.[(triple3)] Charlie is red.[(triple4 OR ((triple3) -> rule3))] Charlie is smart.[(triple5)] Fiona is green.[(triple6)] Fiona is red.[(triple7)] Harry is not cold.[(triple8)] Harry is smart.[(triple9)] Harry is young.[(triple10)] @1: Anne is red.[(((triple1) -> rule3))] Charlie is cold.[(((triple4) -> rule2) OR ((((triple3) -> rule3)) -> rule2))] Fiona is cold.[(((triple7) -> rule2))] @2: Anne is cold.[(((((triple1) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple3) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Harry is not cold.
("Harry" "is" "cold" "-")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2