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