Charlie is blue. Charlie is furry. Charlie is kind. Charlie is quiet. Charlie is young. Dave is blue. Dave is cold. Dave is green. Dave is kind. Dave is quiet. Dave is young. Fiona is blue. Fiona is furry. Fiona is green. Fiona is young. Harry is blue. If Charlie is kind and Charlie is furry then Charlie is young. If Dave is furry then Dave is quiet. All furry, kind things are young. Blue things are young. Green, cold things are kind. Green things are cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Charlie is kind and Charlie is furry then Charlie is young.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "young" "+"))
If Dave is furry then Dave is quiet.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "quiet" "+"))
All furry, kind things are young.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Green, cold things are kind.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Dave is quiet.
True
1
proof
[(triple10)]
("Dave" "is" "quiet" "+")
triple10
Dave is not kind.
False
1
inv-proof
[(triple9 OR ((triple8 triple7) -> rule5) OR ((triple8 ((triple8) -> rule6)) -> rule5))]
("Dave" "is" "kind" "-")
triple9
((triple8 triple7) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Harry is young.
True
2
proof
[(((triple16) -> rule4))]
("Harry" "is" "young" "+")
((triple16) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple16) -> rule4))]
("Harry" "is" "young" "-")
((triple16) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Fiona is kind.
True
4
proof
[(((triple14 ((triple14) -> rule6)) -> rule5))]
("Fiona" "is" "kind" "+")
((triple14 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not kind.
False
4
inv-proof
[(((triple14 ((triple14) -> rule6)) -> rule5))]
("Fiona" "is" "kind" "-")
((triple14 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4)] Charlie is young.[(triple5 OR ((triple1) -> rule4) OR ((triple2 triple3) -> rule3) OR ((triple3 triple2) -> rule1))] Dave is blue.[(triple6)] Dave is cold.[(triple7 OR ((triple8) -> rule6))] Dave is green.[(triple8)] Dave is kind.[(triple9 OR ((triple8 triple7) -> rule5) OR ((triple8 ((triple8) -> rule6)) -> rule5))] Dave is quiet.[(triple10)] Dave is young.[(triple11 OR ((triple6) -> rule4))] Fiona is blue.[(triple12)] Fiona is furry.[(triple13)] Fiona is green.[(triple14)] Fiona is young.[(triple15 OR ((triple12) -> rule4) OR ((triple13 ((triple14 ((triple14) -> rule6)) -> rule5)) -> rule3))] Harry is blue.[(triple16)] @1: Fiona is cold.[(((triple14) -> rule6))] Harry is young.[(((triple16) -> rule4))] @2: Fiona is kind.[(((triple14 ((triple14) -> rule6)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
((triple8) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
((triple8 triple7) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
((triple6) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
Fiona is furry.
("Fiona" "is" "furry" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is young.
("Fiona" "is" "young" "+")
triple15
((triple12) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple13 ((triple14 ((triple14) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple16
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple14) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple16) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple14 ((triple14) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2