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