Charlie is nice. Charlie is smart. Charlie is white. Dave is cold. Dave is kind. Dave is nice. Dave is rough. Dave is round. Dave is smart. Dave is white. Fiona is kind. Fiona is round. If someone is smart and rough then they are white. If Dave is nice and Dave is white then Dave is smart. If someone is round then they are rough. If someone is white then they are round. If Dave is smart then Dave is cold. Nice people are cold.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is smart and rough then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Dave is nice and Dave is white then Dave is smart.
((("Dave" "is" "nice" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "smart" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart then Dave is cold.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "cold" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Dave is kind.
True
1
proof
[(triple5)]
("Dave" "is" "kind" "+")
triple5
Dave is not nice.
False
1
inv-proof
[(triple6)]
("Dave" "is" "nice" "-")
triple6
Charlie is round.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "round" "+")
((triple3) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple12) -> rule3))]
("Fiona" "is" "rough" "-")
((triple12) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "cold" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Charlie is nice.[(triple1)] Charlie is smart.[(triple2)] Charlie is white.[(triple3)] Dave is cold.[(triple4 OR ((triple6) -> rule6) OR ((triple9) -> rule5) OR ((((triple6 triple10) -> rule2)) -> rule5))] Dave is kind.[(triple5)] Dave is nice.[(triple6)] Dave is rough.[(triple7 OR ((triple8) -> rule3) OR ((((triple10) -> rule4)) -> rule3))] Dave is round.[(triple8 OR ((triple10) -> rule4) OR ((((triple9 triple7) -> rule1)) -> rule4))] Dave is smart.[(triple9 OR ((triple6 triple10) -> rule2))] Dave is white.[(triple10 OR ((triple9 triple7) -> rule1) OR ((triple9 ((triple8) -> rule3)) -> rule1))] Fiona is kind.[(triple11)] Fiona is round.[(triple12)] @1: Charlie is cold.[(((triple1) -> rule6))] Charlie is round.[(((triple3) -> rule4))] Fiona is rough.[(((triple12) -> rule3))] @2: Charlie is rough.[(((((triple3) -> rule4)) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple6) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple9) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
((triple8) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple8
((triple10) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple9 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple6 triple10) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple9 triple7) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple9 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple12) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2