Charlie is big. Charlie is cold. Charlie is nice. Charlie is not red. Charlie is rough. Charlie is not young. Dave is big. Dave is cold. Dave is nice. Dave is red. Dave is rough. Dave is smart. Dave is young. Fiona is nice. Fiona is rough. All cold things are smart. If Charlie is nice then Charlie is smart. If Fiona is rough and Fiona is cold then Fiona is not young. If something is smart and not nice then it is big. All young, red things are big. If something is cold and not smart then it is rough. If something is nice and not smart then it is rough. If something is young and not smart then it is not rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Charlie is nice then Charlie is smart.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "smart" "+"))
If Fiona is rough and Fiona is cold then Fiona is not young.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "young" "-"))
If something is smart and not nice then it is big.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
All young, red things are big.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is cold and not smart then it is rough.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "+"))
If something is nice and not smart then it is rough.
((("something" "is" "nice" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "+"))
If something is young and not smart then it is not rough.
((("something" "is" "young" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "-"))
Charlie is not red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Charlie is smart.
True
2
proof
[(((triple2) -> rule1) OR ((triple3) -> rule2))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple3) -> rule2))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is nice.[(triple3)] Charlie is not red.[(triple4)] Charlie is not young.[(triple6)] Charlie is rough.[(triple5)] Dave is big.[(triple7 OR ((triple13 triple10) -> rule5))] Dave is cold.[(triple8)] Dave is nice.[(triple9)] Dave is red.[(triple10)] Dave is rough.[(triple11)] Dave is smart.[(triple12 OR ((triple8) -> rule1))] Dave is young.[(triple13)] Fiona is nice.[(triple14)] Fiona is rough.[(triple15)] @1: Charlie is smart.[(((triple2) -> rule1) OR ((triple3) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Charlie is not young.
("Charlie" "is" "young" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple7
((triple13 triple10) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((triple8) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple13
Fiona is nice.
("Fiona" "is" "nice" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1