Charlie is blue. Charlie is cold. Charlie is red. Charlie is rough. Charlie is smart. Charlie is white. Charlie is young. Fiona is cold. Fiona is rough. Fiona is smart. Fiona is white. Fiona is young. All red, blue things are rough. If Fiona is blue and Fiona is cold then Fiona is red. All smart, young things are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All red, blue things are rough.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Fiona is blue and Fiona is cold then Fiona is red.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
All smart, young things are blue.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Charlie is red.
True
1
proof
[(triple3)]
("Charlie" "is" "red" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple1 OR ((triple5 triple7) -> rule3))]
("Charlie" "is" "blue" "-")
triple1
((triple5 triple7) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is blue.
True
3
proof
[(((triple10 triple12) -> rule3))]
("Fiona" "is" "blue" "+")
((triple10 triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
3
inv-proof
[(((triple10 triple12) -> rule3))]
("Fiona" "is" "blue" "-")
((triple10 triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
True
5
proof
[(((((triple10 triple12) -> rule3) triple8) -> rule2))]
("Fiona" "is" "red" "+")
((((triple10 triple12) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not red.
False
5
inv-proof
[(((((triple10 triple12) -> rule3) triple8) -> rule2))]
("Fiona" "is" "red" "-")
((((triple10 triple12) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
@0: Charlie is blue.[(triple1 OR ((triple5 triple7) -> rule3))] Charlie is cold.[(triple2)] Charlie is red.[(triple3)] Charlie is rough.[(triple4 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple5 triple7) -> rule3)) -> rule1))] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7)] Fiona is cold.[(triple8)] Fiona is rough.[(triple9 OR ((((((triple10 triple12) -> rule3) triple8) -> rule2) ((triple10 triple12) -> rule3)) -> rule1))] Fiona is smart.[(triple10)] Fiona is white.[(triple11)] Fiona is young.[(triple12)] @1: Fiona is blue.[(((triple10 triple12) -> rule3))] @2: Fiona is red.[(((((triple10 triple12) -> rule3) triple8) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple5 triple7) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple3 triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple3 ((triple5 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
((((((triple10 triple12) -> (rule3 % int3)) triple8) -> (rule2 % int2)) ((triple10 triple12) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple10 triple12) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple10 triple12) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2